\documentclass[10pt, a4paper]{article}
\usepackage[paper=a4paper, left=1.5cm, right=1.5cm, bottom=1.5cm, top=3.5cm]{geometry}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[spanish]{babel}
\usepackage{indentfirst}
\usepackage{fancyhdr}
\usepackage{latexsym}
\usepackage{lastpage}
\usepackage{aed2-symb,aed2-itef,aed2-tad}
\usepackage[colorlinks=true, linkcolor=blue]{hyperref}
\usepackage{calc}

\newcommand{\f}[1]{\text{#1}}
\renewcommand{\paratodo}[2]{$\forall~#2$: #1}

\sloppy

\hypersetup{%
 % Para que el PDF se abra a pgina completa.
 pdfstartview= {FitH \hypercalcbp{\paperheight-\topmargin-1in-\headheight}},
 pdfauthor={Grupo 16 - Algoritmos y estructuras de datos II},
 pdfkeywords={TADS},
 pdfsubject={TP I}
}

\parskip=5pt % 10pt es el tamao de fuente

% Pongo en 0 la distancia extra entre temes.
\let\olditemize\itemize
\def\itemize{\olditemize\itemsep=0pt}

% Acomodo fancyhdr.
\pagestyle{fancy}
\thispagestyle{fancy}
\addtolength{\headheight}{1pt}
\lhead{Trabajo Practico I}
\rhead{$1^{\mathrm{er}}$ cuatrimestre de 2012}
\cfoot{\thepage /\pageref{LastPage}}
\renewcommand{\footrulewidth}{0.4pt}

\author{Grupo 16 - Algoritmos y estructuras de datos II}
\date{}
\title{Trabajo Practico I - Tipos abstractos de datos}

\begin{document}

%Pagina de titulo e indice
\thispagestyle{empty}

\maketitle
\tableofcontents

\newpage

%TADS

\section{TAD \tadNombre{RedSocial}}

\begin{tad}{\tadNombre{RedSocial}}
\tadGeneros{redSocial}
\tadExporta{generadores, observadores, mensajesDelMuro, decoraMensajes?, aCuantosDecoraElTag}
\tadUsa{\tadNombre{Bool, Nat, Fecha, Usuario, Mensaje, Imperio, Tag}}

\tadIgualdadObservacional{r}{r'}{redSocial}{imperio(r)$\igobs$imperio(r') $\land$ usuarios(r)$\igobs$usuarios(r') $\land$mensajes(r)$\igobs$mensajes(r') $\land$ amistades(r)$\igobs$amistades(r') $\land$ pedidosDeAmistad(r)$\igobs$pedidosDeAmistad(r')}
\tadAlinearFunciones{mensajesDelMuroAux}{usuario,redSocial,fecha,conj(nombre)}

\tadObservadores 
\tadOperacion{imperio}{redSocial}{imperio}{} 
\tadOperacion{usuarios}{redSocial}{dicc(usuario, pais)}{} 
\tadOperacion{mensajes}{redSocial}{pila(mensaje)}{} 
\tadOperacion{amistades}{redSocial\ $r$, usuario\ $ u$}{conj(usuario)}{ $u$ $\in$ nombresDeUsuarios($r$)} 
\tadOperacion{pedidosDeAmistad}{redSocial\ $r$, usuario\ $ u$}{conj(usuario)}{$u$ $\in$ nombresDeUsuarios($r$)}

\tadGeneradores
\tadOperacion{crearRedSocial}{imperio\ i}{redSocial}{}
\tadOperacion{agregarUsuario}{redSocial\ $r$, usuario\ $u$, pais\ $p$}{redSocial}{$\neg$($u$ $\in$ nombresDeUsuarios($r$)) $\land$ $p$ $\in$ paises(imperio($r$))}
\tadOperacion{agregarMensaje}{redSocial\ $r$, mensaje\ $m$, usuario $u$}{redSocial}{($u$ $\in$ nombresDeUsuarios($r$)) $\land$\ $\neg$(fecha($m$) >\ fechaUltimoMensaje($r$)}
\tadOperacion{enviarSolicitud}{redSocial\ $r$, usuario\ $u$, usuario\ $u'$}{redSocial}{($u$ $\in$ nombresDeUsuarios($r$)) $\land$\ (u' $\in$ nombresDeUsuarios($r$)) $\land$\ $\neg$ (envioSolicitud($r$, $u$, $u'$) $\lor$ envioSolicitud($r$, $u'$, $u$)) $\land$ $\neg$ ($u$ $\in$ amigosDeU($r$,$u'$))}
\tadOperacion{aceptarSolicitud}{redSocial\ $r$, usuario\ $u$, usuario\ $u'$}{redSocial}{envioSolicitud($r$, $u'$, $u$)}

\tadOtrasOperaciones
\tadOperacion{fechaUltimoMensaje}{redSocial}{Nat}{}
\tadOperacion{mensajesDelMuro}{usuario\ u,redSocial\ r}{secu(mensaje)}{def?(u,usuarios(r))}
\tadOperacion{mensajesDelMuroAux}{redSocial\ r, pila(mensaje)\ m, usuario\ u}{secu(mensaje)}{}
\tadOperacion{decoraMensajes?}{usuario\ u, tag\ t, redSocial\ r}{bool}{def?(u,usuarios(r))}
\tadOperacion{decoraMensajesAux}{usuario\ u, tag\ t, redSocial\ r}{bool}{}
\tadOperacion{aCuantosDecoraElTag}{usuario\ u, tag\ t, redSocial\ r}{Nat}{def?(u,usuarios(r)) $\land$L decoraMensajes?(r, mensajes(r), u)}
\tadOperacion{cuantosDecora}{usuario\ u, tag\ t, redSocial\ r}{Nat}{}
\tadOperacion{sinRestricciones}{redSocial\ r, pais\ p, pais\ p', contenido\ c}{bool}{}
\tadOperacion{fechaValida}{redSocial\ r, fecha\ f}{bool}{}



\tadOperacion{envioSolicitud}{redSocial,usuario,usuario}{bool}{}


\tadAxiomas[$\forall$ r:redSocial,$\forall$ u,u':usuario,$\forall$ i:imperio,$\forall$m:mensaje]

\tadAlinearAxiomas{redSocial,usuario,usuario,mensaje,fecha,imperio,imperio}{}

\tadAxioma{imperio(crearRedSocial ($i$))}{$i$}{}
\tadAxioma{imperio(agregarUsuario (($u$, $p$, $r$)))}{imperio($r$)}{}
\tadAxioma{imperio(agregarMensaje ($u$, $m$, $r$))}{imperio($r$)}{}
\tadAxioma{imperio(enviarSolicitud ($u$, $u$', $r$))}{imperio($r$)}{}
\tadAxioma{imperio(aceptarSolicitud ($u$, $u$', $r$))}{imperio($r$)}{}


$\newline$

\tadAxioma{mensajes(crearRedSocial ($i$))}{vacia}{}
\tadAxioma{mensajes(agregarUsuario ($u$, $p$, $r$))}{mensaje($r$)}{}
\tadAxioma{mensajes(agregarMensaje ($u$, $m$, $r$))}{apilar($m$, mensajes($r$))}{}
\tadAxioma{mensajes(enviarSolicitud ($u$, $u$', $r$), $us$)}{mensajes($r$)}{}
\tadAxioma{mensajes(aceptarSolicitud ($u$, $u$', $r$), $us$)}{mensajes($r$)}{}

$\newline$

\tadAxioma{usuarios(crearRedSocial ($i$))}{vacio}{}
\tadAxioma{usuarios(agregarUsuario ($u$, $p$, $r$))}{definir($u$, $p$ , usuarios($r$))}{}
\tadAxioma{usuarios(agregarMensaje ($u$, $m$, $r$))}{usuarios($r$)}{}
\tadAxioma{usuarios(enviarSolicitud ($u$, $u'$, $r$), $us$)}{usuarios($r$)}{}
\tadAxioma{usuarios(aceptarSolicitud ($u$, $u'$, $r$), $us$)}{usuarios($r$)}{}

$\newline$

\tadAxioma{amistades(crearRedSocial ($i$))}{ $\emptyset$ }{}
\tadAxioma{amistades(agregarUsuario ($u$, $p$, $r$))}{amistades($r$)}{}
\tadAxioma{amistades(agregarMensaje ($u$, $m$, $r$))}{amistades($r$)}{}
\tadAxioma{amistades(enviarSolicitud ($u$, $u'$, $r$), $us$)}{amistades($r$)}{}
\tadAxioma{amistades(aceptarSolicitud ($u$, $u'$, $r$), $us$)}{\IF $us$ = $u$ THEN ag($u'$, amistades($r$)) ELSE {\IF $us$ = $u'$ THEN ag($u$, amistades($r$)) ELSE amistades($r$) FI} FI}{}

$\newline$

\tadAxioma{pedidosDeAmistad(crearRedSocial i)}{$\emptyset$}{}
\tadAxioma{pedidosDeAmistad(agregarUsuario ($u$, $p$, $r$))}{pedidosDeAmistad($r$)}{}
\tadAxioma{pedidosDeAmistad(agregarMensaje ($u$, $m$, $r$))}{pedidosDeAmistad($r$)}{}
\tadAxioma{pedidosDeAmistad(enviarSolicitud ($u$, $u'$, $r$), $us$)}{\IF $us$ = $u'$ THEN ag($u$, pedidosDeAmistad($r$)) ELSE pedidosDeAmistad($r$) FI}{}
\tadAxioma{pedidosDeAmistad(aceptarSolicitud ($u$, $u'$, $r$), $us$)}{pedidosDeAmistad($r$)}{}

$\newline$

\tadAxioma{fechaUltimoMensaje(crearRedSocial i)}{0}{}
\tadAxioma{fechaUltimoMensaje(registrar u p r)}{fechaUltimoMensaje(r)}{}
\tadAxioma{fechaUltimoMensaje(agregarMensaje u m r)}{fecha(m)}{}
\tadAxioma{fechaUltimoMensaje(enviarSolicitud u u' r)}{fechaUltimoMensaje(r)}{}
\tadAxioma{fechaUltimoMensaje(aceptarSolicitud u u' r)}{fechaUltimoMensaje(r)}{}

$\newline$

\tadAxioma{mensajesDelMuro(u,r)}{mensajesDelMuroAux(u,r,fechaSemanaBase$\newline$(fechaUltimoMensaje(r)),obtener(u,(amistades(r)))}{}

$\newline$

\tadAxioma{mensajesDelMuroAux(u,(crearRedSocial i),fechaSemanaBase,amigos)}{<>}{}
\tadAxioma{mensajesDelMuroAux(u,(registrar u' p r),fechaSemanaBase,amigos)}{mensajesDelMuroAux(r)}{}
\tadAxioma{mensajesDelMuroAux(u,(agregarMensaje u' m r),fechaSemanaBase,amigos)}{\IF
((u' $\in$ amigos) $\land$ (fecha(m) > fechaSemanaBase) $\land$ $\neg$($\langle$ u',paisDelUsuario(u',usuarios(r)) $\rangle$ $\in$ (obtener(paisDelUsuario(u,usuarios(r)),restricciones(imperio(r)))))) 
THEN
m $\bullet$ mensajesDelMuroAux(u,r,fechaSemanaBase,amigos)
ELSE 
mensajesDelMuroAux(u,r,fechaSemanaBase,amigos)
FI}{}

\tadAxioma{mensajesDelMuroAux(u,(enviarSolicitud u' u'' r),fechaSemanaBase,amigos)}{mensajesDelMuroAux(r)}{}
\tadAxioma{mensajesDelMuroAux(u,(aceptarSolicitud u' u'' r),fechaSemanaBase,amigos)}{mensajesDelMuroAux(r)}{}

$\newline$

\tadAxioma{paisDelUsuario(u,usuarios)}
{\IF $\Pi_1$ dameUno(usuarios) $\igobs$ u THEN $\Pi_2$ dameUno(usuarios) ELSE paisDelUsuario(u, sinUno(usuarios)) FI
}{}

$\newline$

\tadAxioma{decoraMensajes?(u,t,r)}{$\neg$0?(aCuantosDecoraElTag(u,t,r))}{}

$\newline$

\tadAxioma{aCuantosDecoraElTag(u,t,r)}{cuantasVecesSeRepite(t,mensajesDelMuro(u,r))}{}

$\newline$

\tadAxioma{cuantasVecesSeRepite(t,mensajes)}
{\IF vacia?(mensajes) 
THEN 0 
ELSE
	{\IF t == tag(prim(mensajes)) THEN 1 + cuantasVecesSeRepite(t,fin(mensajes)) ELSE 							    cuantasVecesSeRepite(t,fin(mensajes)) FI}
FI
}{}

$\newline$

\tadAxioma{amigosDeU(r,u)}{obtener(u,amistades(r))}{}

$\newline$

\tadAxioma{nombresDeUsuarios(r)}{nombresDeUsuariosAux(usuarios(r))}{}

$\newline$

\tadAxioma{nombresDeUsuariosAux(us)}{\IF vacio?(us) THEN $\emptyset$ ELSE Ag($\Pi_1$dameUno(us),nombresDeUsuariosAux(sinUno(us))) FI}{}

$\newline$

\tadAxioma{fechaSemanaBase(r,fecha)}{\IF fechaUltimoMensa(r) > (7*24*60*60) THEN fechaUltimoMensa(r) - (7*24*60*60) ELSE fechaUltimoMensa(r) FI}{}

$\newline$

\tadAxioma{envioSolicitud(r,u,u')}{def?(u,pedidosDeAmistad(r)) $\land$L u' $in$ significado(u,pedidosDeAmistad(r))}{}

\end{tad}



\newpage

\section{TAD \tadNombre{Imperio}}

\begin{tad}{\tadNombre{Imperio}}
\tadGeneros{imperio}
\tadExporta{ Imperio, Observadores, esCorrecto, losQuePuedenVerlo, noLosPuedeVer }

\tadIgualdadObservacional{i}{i'}{imperio}{restricciones(i)$\igobs$ restricciones(i') $\land$ paises(i)$\igobs$ paises(i')}
%\tadAlinearFunciones{\argumento $\implies$ \argumento}{bool,bool}

\tadObservadores
\tadOperacion{restricciones}{imperio}{dicc(pais, conj(tupla(pais, contenido))}{}
\tadOperacion{paises}{imperio}{conj(pais)}{}

\tadGeneradores

\tadOperacion{crearImperio}{conj(pais)}{imperio}{}
\tadOperacion{restringir}{pais/p_0,pais/p_1,contenido/c,imperio/i}{bool}{$p_0 \in$ paises(i) $\wedge$ $p_1 \in$ paises(i) $\wedge$ $tupla(p1, c) \notin$ obtener(p0, restricciones(i))}

\tadOtrasOperaciones

\tadOperacion{esCorrecto}{imperio}{bool}{}
\tadOperacion{noLosPuedeVer}{pais,contenido,conj(pais),imperio}{bool}{}
\tadOperacion{losQuePuedenVerlo}{pais,contenido,conj(pais),imperio}{conj ($pais$)}{}


\tadAxiomas[\paratodo{bool}{x,y}]
%\tadAlinearAxiomas[]
%\tadAlinearAxiomas{$false \land x$}
\tadAlinearAxiomas{redSocial,usuario,usuario,mensaje,f}{}
%\ \ \ restricciones (crearImperio) $\equiv$ vacio
%\ \ \ restricciones (restringir d h c i) 

\tadAxioma{restricciones (crearImperio)}{vacio}
\tadAxioma{restricciones (restringir ($d$, $h$, $c$, $i$))}{ \IF def?($d$) THEN definir($d$, ag($\langle$ $h$, $c$ $\rangle$, obtener($d$, restricciones ($i$))), borrar($d$, restricciones ($i$))) ELSE definir ($d$, ag($\langle$ $h$, $c$ $\rangle$, vacio)) FI}
\vspace{1cm}

\tadAxioma{paises(crearImperio c)}{c}
\tadAxioma{paises (restringir ($d$, $h$, $c$, $i$))}{paises ($i$)}
\vspace{1cm}

\tadAxioma{esCorrecto (crearImperio ($p$))}{$True$}
\tadAxioma{esCorrecto (restringir ($d$, $h$, $c$, $i$))}{noLosPuedeVer ($d$, $c$, losQuePuedenVerlo ($h$, $c$, paises ($i$), $i$), $i$) \&\& esCorrecto($i$)}
\vspace{1cm}

\tadAxioma{noLosPuedeVer ($p$, $c$, $cp$, $i$)}{ $cp$ $\subseteq$ (obtener( $p$, restricciones ($i$))) }

\vspace{1cm}

\tadAxioma{losQuePuedenVerlo ($p$, $c$, $cp$, $i$)}{ \IF vacio?($ps$) THEN vacio \\ ELSE  {\IF ( $\langle$ $h$, $c$ $\rangle$ $\in$ obtener( dameUno ($p$), restricciones($i$)) ) \\ THEN losQuePuedenVerlo($h$, $c$, sinUno($ps$), $i$) ELSE Ag( $\langle$ dameUno($ps$), $c$ $\rangle$ , losQuePuedenVerlo($h$, $c$, sinUno($ps$), $i$) ) FI} FI}

\end{tad}

$\newline$

\section{TAD \tadNombre{Mensaje}}

\begin{tad}{\tadNombre{Mensaje es Tupla(string, contenido, tags, fecha)}}

\end{tad}

\section{TAD \tadNombre{Usuario}}

\begin{tad}{\tadNombre{Usuario es String}}

\end{tad}


\section{TAD \tadNombre{Fecha}}

\begin{tad}{\tadNombre{Fecha es Nat}}

\end{tad}


\section{TAD \tadNombre{Tag}}

\begin{tad}{\tadNombre{Tag es String}}

\end{tad}


\section{TAD \tadNombre{Contenido}}

\begin{tad}{\tadNombre{Contenido es enum(Video, Texto, Foto, Audio)}}

\end{tad}


\section{TAD \tadNombre{Pais}}

\begin{tad}{\tadNombre{Pais es String}}

\end{tad}



\end{document}
